1 EXISTENCE AND UNIQUENESS OF HAAR MEASURE 245 Properties (i), (ii), and (iii) are immediate consequences of the definitions. Given (14.1.5.1), there exists (3.17.10) s e G such that sup /(x) = /CO £ Z cig(sr 's) ^ ( Z c*) sup g(x), xeG i=l \i=l / jceG and (iv) follows. For (v), observe that if we have /^ZaiY(X')# anc* 9 = Z */Y(0)^> then/g £ aibjy(sitj)h, and therefore J i, J i,j Since we may take Z#i (resp. J^bj) arbitrarily close to (/: g) (resp. (g: h)), we have (v). Finally, (vi) follows from (v) applied to/0, / g and to / f0, g. By hypothesis, there exists a denumerable fundamental system (Vn) of neighborhoods of the neutral element e in G. For each n, \ttgn be a function belonging to «2f* such that Supp(#rt) <=zVn (4.5.2). Let/0 be a function in Jf * , fixed once and for all, and put (14.1.5.2) !„(/) = (/: gn)j(fQ : gn) for all fe tf * ; let In(0) = 0. From (ii) and (iii) above it follows immedi- ately that the mappings /-*!„( |/|) are seminorms on ^TR(G), and from (i) that ln(y(s)f) = !„(/) for all s e G. Next, there exists a sequence of relatively compact open sets Up which cover G and are such that Op c Up+1 (3.18.3). The space ^(Up) is separable (7.4.4) and therefore so is ^f(G; Op) n Jf * (3.10.9). Hence there exists a dense sequence (fmp)m*i in the latter space. Since the sequence of values ln(fmp) (n ^ 1) lies in the compact interval with endpoints l/(/0 :fmp) and (fmp :/o) by (vi), it follows from (12.5.9) that if we replace the sequence (gn) by a suitably chosen subsequence, we may assume that the sequence (ln(fmp))nzi tends to a limit >Qfor all m, p. Also it is clear that if/,/' in Jf" * are such that/^/', then !„(/) :g !„(/')• Let hp be a continuous mapping of G into [0, 1] with compact support, taking the value 1 on Op ((3.18.2) and (4.5.2)). Then, for each function/e jf (G; Op) n Jf * , we have !„(/) g ||/|| \n(hp) for all /i, and therefore for all//' e ^f(G, Up) n ^f + and all «, because/i-^In( |/j) is a seminorm. In other words, the set of restrictions of the !„ to each of the subspaces JT(G, Up) n jf ^ is equicontinuous. By (7.5.5) it follows that lim !„(/) = !(/) »-+oo exists for all/6 Jf *, and takes values ^0. is called the Bernoulli scheme B(j?0 , • • • > Pm- 1).